(declare-sort S0 0)

(declare-sort S1 0)

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const i0 Int)
(declare-const i4 Int)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r7 Real)
(declare-const r9 Real)
(declare-const r10 Real)
(declare-const r12 Real)
(declare-const r13 Real)
(declare-const r16 Real)
(declare-const _10-0 (_ BitVec 10))
(declare-const v10 Bool)
(assert v10)
(declare-const r18 Real)
(assert (and (>= 5 i4) v7 v4 v1 v2 v6 v9 v4 v8 v3 v0))
(assert (= v8 (= _10-0 _10-0 _10-0) (> r13 r9) v8 v4 v0 v1 v1))
(declare-const r19 Real)
(declare-const _12-0 (_ BitVec 12))
(declare-const r20 Real)
(declare-const v11 Bool)
(declare-const i5 Int)
(assert (or (=> (= v8 (= _10-0 _10-0 _10-0) (> r13 r9) v8 v4 v0 v1 v1) (is_int (to_real i4))) v8 (=> (= v8 (= _10-0 _10-0 _10-0) (> r13 r9) v8 v4 v0 v1 v1) (is_int (to_real i4))) (= _10-0 _10-0 _10-0) (= v8 (= _10-0 _10-0 _10-0) (> r13 r9) v8 v4 v0 v1 v1)))
(declare-const i6 Int)
(declare-const r21 Real)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const r22 Real)
(declare-const v14 Bool)
(declare-const v15 Bool)
(assert v5)
(declare-const v16 Bool)
(declare-const i7 Int)
(assert (= (bvnand _10-0 (bvshl _10-0 _10-0)) (bvshl _10-0 _10-0)))
(assert v2)
(assert (exists ((q0 S1) (q1 (_ BitVec 1)) (q2 (_ BitVec 10)) (q3 Real)) (xor (distinct q0 q0 q0) (distinct q1 ((_ extract 4 4) (bvnand _10-0 (bvshl _10-0 _10-0))) q1 q1 (bvcomp ((_ extract 4 4) (bvnand _10-0 (bvshl _10-0 _10-0))) (bvxor ((_ extract 4 4) (bvnand _10-0 (bvshl _10-0 _10-0))) ((_ extract 4 4) (bvnand _10-0 (bvshl _10-0 _10-0)))))) (<= 921825204.5 q3 r7) (bvule q2 (bvshl _10-0 _10-0)))))
(check-sat)
